$\forall$$k$:Knd, $l$:IdLnk, ${\it ds}$:$x$:Id fp$\rightarrow$ Type, $A$, $T$:Type, ${\it tg}$:Id, $f$:(State(${\it ds}$)$\rightarrow$$A$$\rightarrow$$T$).
\\[0ex]$k$(v) sends [${\it tg}$,$f$(State(${\it ds}$), v)] on $l$ $\in$ Realizer